P51 · Lighting a unit square · Discussion

[证明思路 · p51-n2-v1] 本题n=2时证明思路

NUE_13

关联子题: https://minmaxarena.com/problems/lights-in-a-square/p51-n2-v1 此为投稿,数学正确性与最优性尚待审核。 可以分成2个1*0.5的长方形,2点均在中间的剪切轴。 然后针对三个特殊情况(对另一边中点的距离和两点分别对另一边的左右两端的距离)计算光强,并列出两个用于计算光强的函数,分别是mid(x)和side(x),其中x为这两个点的距离。(0<=x<=0.5) 随后算出min(mid(x),side(x))的最大值,即为最大光强。 此时再用对应的x直接算出两点的距离即可。

NUE_13

证明思路又补充了一下: 这里的“照明”特指最低亮度,所以最重要的是所有地方都能照亮,而不是平均亮度和最大亮度,所以为了正方形能够使最暗的地方照亮,所以两个点离任何一点都不能太远,特别是角落。因此,为了不使两点离角落太远,绝不能有一点靠某个角落或某个地方太近。另外,为了使两点照到的亮度相对平均,应该呈对称型。因此,可以得出,两点沿正方形的一条非对角线对称轴对称,且两点在另一条非对角线对称轴上。之后,就可以以两点所在的线分割为上下两部分,因为两部分都对称,所以只需考虑一部分就行了,这之后就是我提出的证明思路了。至于为什么只看中点和两边顶点,这是因为这两个是特殊值,中点很好理解,是因为两个点都在慢慢远离中点;而顶点的原因前文也有说过。因为“一点的光强是各光源到它距离平方的倒数之和”,可以把mid(x)和side(x)表示出来:mid(x)=2/(0.25+x^2/4),side(x)=1/(0.25+(1-x)^2/4)+1/(0.25+(x+1)^2/4),其中x为两个光源的距离。由于两个函数中取的是“最暗的那一点”,因此两个函数中无论某一点多亮,都只看最小值,因而正数的最高值即为两函数图像的交点,即mid(x)=side(x)。DeepSeek-V4-Pro给出了x=sqrt(6)/3,我自己也在GeoGebra画图网站上验证了一下。对应的光强则恰好等于4.8,但由于精度问题,验证器只能显示4.799999。 (邮件已发送,这里再发一次)

SneakyZero

谢谢补充。按你写的对称参数化,x=√6/3 代入 mid、side 的确都得到 4.8,这很好地解释了这个候选构型。这里 x 是两个光源的间距,√6/3≈0.8165,所以正文的 0≤x≤0.5 与这套公式不一致,需要先统一。 完整最优性证明还缺两个关键步骤:一是证明任意布局都不会优于这种轴对称布局,不能仅由容器对称推出最优构型必然对称;二是证明该构型在整个正方形上的最低光强确实由所检查的点控制。若未证明第二步,只检查中点和角点只能提供有限采样约束。 4.8 已是本题引用的外部已知值;4.799999 与它的差异不能单凭显示解释为最优性证明。我们先保留这份有价值的推导,暂不发完整证明的采纳加分;若补上上述全局论证,会继续核验。

NUE_13

这里正文的0<=x<=0.5我最开始想的是两点距离中点的共同距离,不过后来感觉有点麻烦,所以弃用了,改成了两点的距离。因此正文里的改为0<=x<=1(同时也感谢指出的错误)

NUE_13

第一个步骤暂时空着。关于第二个关键步骤,可以设一个函数dlight(x,d)=1/((d-(1-x)/2)^2+1/4)+1/((x-d+(1-x)/2)^2+1/4)来计算边上各点的光强(0≤x≤1, 0≤d≤1),其中x是两光源的距离,d是计算光强那点的x坐标(示意图一会邮件发)。而要证明的就是在x固定的情况下,只有d=0,1/2和1时会出现函数最小值。我使用DeepSeek-v4-pro证明了它,方法是:首先化简,并通过对称性证明可直接研究0≤d≤1/2部分。随后使用导数分类讨论等一系列方法证明dlight函数在[0,1/2]上要么单调递增,要么先增后减。因此,最小值不可能在区间内部取得,只有在端点d=0、d=1/2处取得。最后根据对称性推广至d=1/2、d=1,因此命题成立。这就解释了为什么只需要检查中点(d=1/2)和角点(d=0或1),第二个关键步骤就得到了解决。第一个关键步骤我试图让AI解决,但不知是不是因为token不够还是提示词不对,这个问题最终失败了。这个我以后解决。

NUE_13

关键步骤1似乎有了思路:因为两点确定一条直线,所以可以把两个点直接连成一条线,然后假设这条线是一整排光源。接下来可以做1*1正方形的内接圆,接下来只看圆,这排光源就相当于单位圆的一条弦,将圆分为两条弧,也就是优弧和劣弧。明显,除非这条弦是直径,劣弧长一定大于优弧,自然劣弧上面最远的点就肯定比优弧远,所以只有这条弦是直径才能使劣弧和优弧长度相等。推出了直径,我们就可以把正方形加入进来了。由于这条光源组成的线是直径,因此它肯定经过圆心,也就是正方形的中心。这条完整的线就会增加正方形中未被覆盖的一部分。现在把这条线段再做为圆的直径,它的长度就一定大于等于1。如果要最小化圆上的最低亮度,那么这条的长度就必然等于1,也就是这条直径必须是这个圆刚好和正方形相切的两个对应点组成的,也就是正方形的一条非对角线对称轴。这就解释了为什么两个点必须在这条线上。

NUE_13

最后关于为何对称,其实是较为明显的。不对称一般有两种情况:两点在同一侧,也就是两点在中点的同一侧。这时离两点较远的顶点的光强一定不会到达4(两点都在中心),与4.8差得很远。而第二种情况则是两点不在中点的同一侧,这时可以再构造出一个对称型(详见邮件),并可以使用第一个回复中mid(x)和side(x)的方式。但是因为不对称,所以这个对称型肯定无法覆盖整个长方形,因此会多出来一截,这里的亮度会比对称部分的低,自然不可能出现最亮。更详细的函数运算这里就先不说了,详见邮件。

SneakyZero

谢谢继续补充。第二步确实有进展:在“两盏灯位于水平中线且关于中心对称”的构型族内,可以严格证明只需检查上下边中点和四个角,并得到该构型族的精确最优值 24/5 = 4.8。 补一个较简洁的验证:设灯在 (1/2−a,1/2)、(1/2+a,1/2),0≤a≤1/2。固定横坐标,把观察点移到上边或下边,会同时增大到两盏灯的距离,所以全域最暗点可在这两条边上寻找。令 u=(d−1/2)²、c=a²+1/4,边上的亮度为 F(u)=2(u+c)/[(u+c)²−4a²u],0≤u≤1/4。 求导得到 F′(u)=2[4a²c−(u+c)²]/[(u+c)²−4a²u]²。 导数分子随 u 严格递减,因此内部驻点只能是极大值,最小值必在 u=0 或 1/4,即边中点或角点。 接着令 v=a²,两种亮度分别为 2/(v+1/4) 和 (2v+1)/(v²+1/4)。当 v≥1/6,前者≤24/5;当 v≤1/6,后者≤24/5(相减可因式分解为 (6v−1)(4v−1)/[5(v²+1/4)]≥0)。在 a=1/√6 时两者同时等于 24/5,灯间距就是 √6/3。这样,第二步可以完整闭合。 目前仍缺的是第一步:为什么任意两灯布局都不可能超过 4.8。最新的“内切圆/整条线发光”论证还不能完成这一步:正方形还包含圆外区域和角点;两盏点光源换成发光线改变了模型,必须给出明确的亮度比较不等式,才能用于原问题。“非对称会多出较暗的一条区域”也需要定量证明该处亮度一定不超过 4.8,而不仅是相对别处更暗。 下一步可以尝试二选一:① 对任意两灯位置,证明正方形内总存在一点亮度≤24/5;② 证明任意布局都能变为上述对称布局,且最小亮度不下降。只需证明存在一个对称最优解,不必证明所有最优解都对称。 所以当前可以确认“对称构型族内最优”的部分结果,但还不能据此认定全局最优。你提到邮件中有详细计算;方便的话请把第一步的关键不等式和推导也贴在这里,便于逐项核验。

NUE_13

啊啊啊啊啊啊啊啊啊……

NUE_13

不过下一步目前已经有了突破。我在2选1中选择了1,然后让DeepSeek-v4-pro证明。我首先让它证明了总存在一点亮度≤8;然后又压缩至5.5,并且已经发现可能有4.8这个更进一步的解。

NUE_13

4.8终于被证出来了!!!啊啊啊!!!(详见邮件,最优性也已说明)

NUE_13

邮件我看到了(我又被AI骗了…… 不过现在的问题似乎已经比之前少得多了。AI缺少的部分,可以再次使用dlight-mid-side三函数的对称构型重新得到,这样就把AI声称的“只取角点”变成了“取角点和中点中的最小”。这样可以优化补全为4.8,也就是对称构型内的最优。而使用AI的反证法,似乎可以容易地证明这就是全局最优。