Skip to content

Improve lower bound for C_71 to 6.4901128435233943#94

Open
463464q435q43 wants to merge 4 commits into
teorth:mainfrom
463464q435q43:improve-71-lower-bound
Open

Improve lower bound for C_71 to 6.4901128435233943#94
463464q435q43 wants to merge 4 commits into
teorth:mainfrom
463464q435q43:improve-71-lower-bound

Conversation

@463464q435q43

@463464q435q43 463464q435q43 commented Jun 10, 2026

Copy link
Copy Markdown

Summary

This updates the best known lower bound for the Fourier Entropy-Influence constant from

$$C_{71} > 6.4547837$$

(Hod 2017, arXiv:1711.00762, Theorem 4.4:
$C \ge \beta(1/2) > 6.4547837$, via a limit of read-once monotone formulas) to

$$C_{71} > 6.4901128435233943,$$

an improvement of +0.0353291435233943 over the table value (second decimal place;
the certified margin over the full record value $\beta(1/2)$ itself is
+0.0353291269606358 — both margins downward-truncated, hence themselves certified).
The full floor-truncated certified value is

$$C_{71} \ge 6.49011284352339435967722960726821776674269968263998854502375.$$

The headline function (14 variables) is logic-monotone (verified
exhaustively), and the O'Donnell–Tan amplification family of a monotone seed is
monotone throughout, so the same certificate also improves the monotone-class
record (Hod's Theorem 4.4 holds even restricted to monotone functions, and so
does this bound):

$$C_{71} > 6.4901128435233943 \quad\text{even restricted to monotone functions.}$$

One object, both claims — no orientation caveat is needed (the table is monotone
exactly as shipped).

Conventions are exactly those of the 71a.md page: $f:{-1,1}^n \to {-1,1}$,
$H(\hat f^2) = \sum_{S\subseteq[n]} \hat f(S)^2 \log_2 (1/\hat f(S)^2)$ (all $S$,
including $S=\emptyset$), $\mathrm{Inf}(f) = \sum_S \hat f(S)^2,\lvert S\rvert$
(= average sensitivity), Fourier coefficients under the uniform measure.

Four earlier, independently certified functions are included as secondary
exhibits (they document the discovery ladder and give the reviewer smaller or
independent instances to check): $g_{12}^{\star}$ on 12 variables, logic-monotone,
certifying $C_{71} > 6.4760668283689727$ even restricted to monotone functions
(the previous headline of this PR; full floor-truncated value
$6.47606682836897279657734782555743832480092248239414132791560$); $g_{12}$ on 12 variables, logic-monotone,
certifying $C_{71} > 6.4742055150632609$ even restricted to monotone functions
(the previous headline of this PR; full floor-truncated value
$6.47420551506326097672878905526134366478869341423326622617201$); $g_{11}$ on
11 variables certifying $C_{71} > 6.4677460490320769$ (not monotone; full
floor-truncated value
$6.46774604903207696483653989653517242017762893521060811040418$); and $g_{10}$
on 10 variables, logic-monotone, certifying $C_{71} > 6.4593722816378557$ even
restricted to monotone functions (full floor-truncated value
$6.45937228163785573157436161221912416621861332113900446566553$). All four are
strictly superseded by the 14-variable headline $g_{14}$ (the
adversarial audit confirms the supersession itself as an exact rational
comparison: $C_{\mathrm{lo}}(g_{14}) - C_{\mathrm{hi}}(g_{12}^{\star}) =
+1.4046\cdot 10^{-2} > 0$, lower endpoint of the new enclosure against the
UPPER endpoint of the old one).

Relation to Hod's construction (attribution)

The incumbent record is Hod's (arXiv:1711.00762, Theorem 4.4: a double-limit of
read-once monotone lexicographic-type formulas). The present construction is not
Hod's family and does not modify it
: the new objects are explicit finite balanced
truth tables found by annealing (details below), fed through the standard
O'Donnell–Tan amplification (arXiv:1304.1347, Lemma 5.1; quoted by Hod as his
Proposition 1.2) — the same mechanism as the page's existing 6.278944 entry
[OT2013]. All credit for the incumbent record and for the amplification framework
belongs to Hod and to O'Donnell–Tan respectively; the new content here is the five
seed functions and their machine-checkable certificates.

New bound

[VARIANT A — finite-stage explicit functions.]

The headline object is an explicit balanced, logic-monotone function
$g_{14}$ on $n = 14$ variables (truth table given below), with exact
total influence

$$\mathrm{Inf}(g_{14}) = \tfrac{521}{256}$$

(integer Walsh–Hadamard transform; the spectral weights $w_S = \hat f(S)^2$ are
exact rationals with denominator $4^n$) and certified spectral entropy

$$H(\hat g_{14}^2) \in [6.718280873178513692634632210648,\ 6.718280873178513692634632210649]$$

(interval arithmetic at 130 decimal digits; true interval width $< 10^{-126}$, the
30-digit endpoints above are floor/ceil truncations of it). It is exactly
balanced
: $\hat f(\emptyset) = 0$, verified as the integer identity
$\sum_x f(x) = 0$ (8192 of 16384 inputs map to TRUE), and logic-monotone:
flipping any input FALSE→TRUE never turns the output TRUE→FALSE, verified
exhaustively over all $14 \cdot 2^{13} = 114688$ comparable input pairs (and
independently over all $3^{14}$ subset-comparable pairs in the audit trail).

The secondary exhibits $g_{12}^{\star}$ ($n = 12$, the previous headline of this
PR), $g_{12}$ ($n = 12$), $g_{11}$ ($n = 11$) and $g_{10}$ ($n = 10$) have exact
influences

$$\mathrm{Inf}(g_{12}^{\star}) = \mathrm{Inf}(g_{12}) = \tfrac{259}{128}, \qquad \mathrm{Inf}(g_{11}) = \tfrac{129}{64}, \qquad \mathrm{Inf}(g_{10}) = \tfrac{257}{128}$$

($g_{12}$ and $g_{12}^{\star}$ share the same exact influence but are distinct
tables — verified entry-by-entry in the audit) and certified spectral entropies

$$H(\hat g_{12}^{\star,2}) \in [6.627849644658870596497129415218,\ 6.627849644658870596497129415219],$$ $$H(\hat g_{12}^2) \in [6.625944706822556155870870048744,\ 6.625944706822556155870870048745],$$ $$H(\hat g_{11}^2) \in [6.568804581048203167412110832418,\ 6.568804581048203167412110832419],$$ $$H(\hat g_{10}^2) \in [6.509836127588151479477286312314,\ 6.509836127588151479477286312315],$$

all exactly balanced by the same integer identity (2048 of 4096 twice, 1024 of
2048, resp. 512 of 1024 inputs map to TRUE). $g_{12}^{\star}$, $g_{12}$ and
$g_{10}$ are logic-monotone exactly as $g_{14}$ is (same exhaustive check).

Amplification (the only theorem used). O'Donnell–Tan (arXiv:1304.1347),
Lemma 5.1, as quoted verbatim by Hod (arXiv:1711.00762) as Proposition 1.2:

Let $g$ be a balanced Boolean function such that $H[g] > 0$. Then any constant
$C$ in [the FEI conjecture] satisfies $C \ge H[g]/(I[g]-1)$.

Derivation chain, with each hypothesis verified exactly (this is the audit's
independent re-derivation; we do not take the formula on faith): for balanced
inner functions on disjoint variables, every Fourier character of the composition
$F(g_1,\dots,g_k)$ factors uniquely as $\chi = \prod_{i\in S}\chi_{T_i}$ with
$T_i \neq \emptyset$ (uniqueness because the copies are variable-disjoint; no
$T_i = \emptyset$ terms because $\hat g(\emptyset) = \mathbb E[g] = 0$). Hence
there are no character collisions and the exact identities
$H[F\circ g] = H[F] + I[F],H[g]$ and $I[F\circ g] = I[F],I[g]$ hold. Iterating
$f_m = g(f_{m-1},\dots,f_{m-1})$ (disjoint copies, $f_0 = g$) gives, for balanced
$g$,

$$\frac{H[f_m]}{I[f_m]} = \frac{H[g]}{I[g]-1}\left(1 - I[g]^{-m}\right) \nearrow \frac{H[g]}{I[g]-1},$$

each $f_m$ a genuine finite Boolean function, every composition level again
exactly balanced. Hypotheses, verified exactly for all five seeds:

  • exact balance: $\sum_x f(x) = 0$, integer check (kills $\hat g(\emptyset)$
    and keeps every composition level balanced);
  • $H > 0$: certified $H > 6.5$ for all five seeds (interval lower endpoints
    above);
  • $I > 1$: $I - 1 = 265/256$ (headline), resp. $131/128$ (twice), $65/64$,
    $129/128$, exact rationals $> 0$ (balanced $\Rightarrow I \ge 1$ with equality only for
    dictators, which have $H = 0$ — Hod's remark after Prop 1.2, re-verified).

The denominator is $(I-1)$, not $I$ — confirmed three ways (OT Lemma 5.1, Hod
Prop 1.2, independent derivation above); the raw ratios $H/I$ of the seeds are
only $\approx 3.301$, $3.276$, $3.275$, $3.26$, $3.24$ and are never quoted as bounds.
Exact rational division of the certified $H$ intervals by the exact $I-1$ gives

$$\frac{H[g_{14}]}{I[g_{14}]-1} \ge 6.49011284352339435967722960726821776674269968263998854502375,$$

and for the secondary exhibits

$$\frac{H[g_{12}^{\star}]}{I[g_{12}^{\star}]-1} \ge 6.47606682836897279657734782555743832480092248239414132791560,$$ $$\frac{H[g_{12}]}{I[g_{12}]-1} \ge 6.47420551506326097672878905526134366478869341423326622617201,$$ $$\frac{H[g_{11}]}{I[g_{11}]-1} \ge 6.46774604903207696483653989653517242017762893521060811040418,$$ $$\frac{H[g_{10}]}{I[g_{10}]-1} \ge 6.45937228163785573157436161221912416621861332113900446566553,$$

all floor-truncated lower endpoints, all $> \beta(1/2)$ by exact rational
comparison against a certified upper enclosure of $\beta(1/2)$ (not merely against
the published decimal 6.4547837).

Monotone-class bound (carried by the headline itself). The shipped
$g_{14}$ table is logic-monotone as encoded — no reorientation, no
negation: flipping any input FALSE→TRUE never turns the output TRUE→FALSE,
verified exhaustively over all $114688$ comparable input pairs by the embedded
script below and by every checker in the trail. Composition of monotone
functions is monotone, so the entire amplification family ${f_m}$ built from
$g_{14}$ is monotone, and

$$C \ge \frac{H[g_{14}]}{I[g_{14}]-1} > 6.4901128435233943 \quad\text{restricted to monotone functions},$$

like Hod's Theorem 4.4 — the general and monotone records coincide in this one
certificate. Of the secondary exhibits, $g_{12}^{\star}$ (the previous headline)
and $g_{12}$ are likewise logic-monotone exactly as shipped (same exhaustive
$24576$-pair check at $n = 12$), and $g_{10}$ is logic-monotone as
shipped (verified over all $5120$ comparable pairs; one transparency note: the
search originally produced it in the input-negated orientation, and the table in
c71_certificate_n10.json is the global input negation
$tt'[x] = tt[x \oplus 1023]$, the monotone representative — $H$, $I$ and balance
are invariant under input negation, so the certificate values are identical for
both orientations). $g_{11}$ carries no monotone claim (it is not monotone
in any orientation; exhaustively checked).

The objects (truth tables — these ARE the construction)

Structural note, stated up front: these are genuinely new annealed truth
tables, not members of any known family
. Total influence is an NPN invariant,
and $521/256$, $259/128$ (twice, two distinct tables), $129/64$, $257/128$ match
no known FEI seed (Hod's $g_m/g'm$ family has
$I = (5-2^{3-2m})/3 \in {3/2, 13/8, 53/32, 213/128, 853/512,\dots}$; balanced
lexicographic functions are dictators with $H = 0$; majorities, tribes,
and parities all mismatch). Their spectra have full-degree support (4542, 1361, 2176,
1052, resp. 738 nonzero coefficients) with a smooth, near-geometric level-weight
decay ($w_1 \approx 0.447$, $w_2 \approx 0.267$, $w_3 \approx 0.159$,
$w_4 \approx 0.083$ for the headline; ratio $\approx 0.6$ per level) matching no
read-once or lexicographic object — "maximum entropy at fixed influence"
structures. The headline $g
{14}$ was found by the same
anneal-plus-greedy-polish search over balanced logic-monotone tables (moves:
(maximal-FALSE, minimal-TRUE) pair swaps, which preserve balance and
monotonicity exactly), run at $n = 14$ and warm-started from the then-certified
incumbent $g_{12}^{\star}$ padded by two variables (2026-06-11); $g_{12}^{\star}$
was found by the same search in an overnight record-extension burst
(2026-06-10/11) warm-started from the then-certified incumbent $g_{12}$ — rank 0
of 88 records from the full 600-minute run; $g_{12}$ itself was found by that
search warm-started from the certified $g_{10}$ monotone winner padded up;
$g_{11}$ and $g_{10}$ were found by simulated
annealing on a biased-measure score functional, then rebalanced by 2 (resp. 4)
greedy truth-table flips to exact balance. This provenance is discovery narrative
only — the certificates rest solely on the explicit tables below and Prop 1.2.

Canonical encoding (Hod's): index $x \in [0, 2^n)$; bit $i$ of $x$ set means
$x_{i+1} = -1 = \mathrm{TRUE}$. The hex strings are the TRUE-set bitmasks (bit $x$
of the integer set $\iff f(x) = -1$); SHA-256 is over the comma-joined decimal
$\pm 1$ truth table string.

$g_{14}$ ($n=14$, headline, logic-monotone; $I = 521/256$; sha256
80929c1b10f4941ba56f13dd355ebaa4c2fabb602df9125a68755c116859d527):

fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00
fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000
fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00
fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000
fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00
fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000
fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00
fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000
fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00
fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000
fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00
fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000
fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00
fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000
fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00
fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000
fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00
fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000
fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00
fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000
fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00
fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000
fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00
fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000
fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00
fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000
fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00
fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000
fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00
fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000
fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00
fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000
fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00
fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000
fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00
fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000
fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00
fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000
fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00
fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000
fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00
fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000
fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00
fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000
fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00
fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000
fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00
fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000
fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00
fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000
fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00
fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000
fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00
fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000
fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00
fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000
fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00
fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000
fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00
fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000
fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00
fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000
fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00
fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000

$g_{12}^{\star}$ ($n=12$, secondary, logic-monotone; $I = 259/128$; sha256
35438a105857623fbd9fdcbee353b9e34b7de683d1132be37f3b1a40346cf714):

fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00
fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000
fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00
fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000
fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00
fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000
fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00
fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000
fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00
fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000
fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00
fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000
fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00
fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000
fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00
fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000

$g_{12}$ ($n=12$, secondary, logic-monotone; $I = 259/128$; sha256
ff94bc3b5fc2ea3a8fd3e6620588dda972ac7b6366e8c7597936535cd0543adb):

fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00
fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000
fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00
fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000
fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00
fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000
fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00
fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000
fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00
fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000
fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00
fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000
fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00
fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000
fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00
fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000

$g_{11}$ ($n=11$, secondary; $I = 129/64$; sha256
2547edf8ac052babfc87b42ab7a402330258d6a9533c542dd8cef449da630383):

f0f33337f7f000f000f555f555f000f0f0f7f7f7f7f0033557f0033557f00337
f7f33337f7f007f557f557f557f007f7f7f7f7f7f7f000000000000000000000
f0f33337f7f000f000f555f555f000f0f0f7f7f7f7f0033557f0033557f00335
f7f33337f7f007f557f557f557f007f5f7f7f7f7f7f000000000000000000000
f0f33337f7f000f050f555f555f000f0f0f777f7f7f0033557f0033557f00337
f7f33337f7f007f557f557f557f007f7f7f777f7f7f000000000000000000000
f0f33337f7f000f050f555f555f000f0f0f777f7f7f0033557f0033557f00335
f7f33337f7f007f557f557f557f007f5f7f777f7f7f

$g_{10}$ ($n=10$, monotone representative; $I = 257/128$; sha256
2ec326a08661bdae8a2f830906bacd1cfa68cd17e767afd736848cbc6e4edf9f):

fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00
fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000
fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00
fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000

Exact data: $\hat f(\emptyset) = 0$ for all five; nonzero spectral weights: 4542
($g_{14}$), 1361 ($g_{12}^{\star}$), 2176 ($g_{12}$), 1052 ($g_{11}$) and 738
($g_{10}$) sets; Parseval $\sum_S w_S = 1$ exact. Machine-readable certificates
(full integer spectra, exact influences, floor-truncated entropy/ratio digit
strings): c71_certificate_n14.json (headline; its truth table ships alongside
as c71_input_table_n14.json, bound to the certificate by the SHA-256 above),
certificate_burst_n12_overnight.json (with the official verifier's own output
verifier_cert_burst_n12_overnight.json), c71_certificate_n12.json,
c71_certificate_n11.json, c71_certificate_n10.json (attached:
gist).

Verification

The certificate is self-verifying. The only transcendental step is $\log_2$,
enclosed with mpmath interval arithmetic; all comparisons against
$6.4547837166 = 64547837166/10^{10}$ (a certified strict upper bound on
$\beta(1/2)$, hence stronger than the page's bar $6.4547837$) are exact rational
comparisons of interval endpoints. The reported bounds are floor-truncations of
the LOWER endpoints, hence rigorous lower bounds on $C_{71}$.

#!/usr/bin/env python3
"""check_c71.py -- self-contained verifier for five new C_71 (FEI) lower bounds.

    C_71 >= 6.49011284352339435967722960726821776674269968263998854502375   (n=14 seed
            g14, logic-monotone -- headline AND monotone-class bound from one object)
    C_71 >= 6.47606682836897279657734782555743832480092248239414132791560   (n=12 seed
            g12*, logic-monotone)
    C_71 >= 6.47420551506326097672878905526134366478869341423326622617201   (n=12 seed,
            logic-monotone)
    C_71 >= 6.46774604903207696483653989653517242017762893521060811040418   (n=11 seed)
    C_71 >= 6.45937228163785573157436161221912416621861332113900446566553   (n=10 seed,
            logic-monotone)

Standalone: Python 3.9+ and mpmath only; zero repository imports. Derived from
the project's checker_template.py (finite mode), certificates inlined.

CONVENTION (matches constants/71a.md, ODWZ 2011, Hod arXiv:1711.00762):
  * f : {-1,+1}^n -> {-1,+1}; TRUE = -1 (Hod). Truth-table encoding: index
    x in [0, 2^n); bit i of x set <=> x_{i+1} = -1 = TRUE.
  * fhat(S) = E_x[f(x) chi_S(x)], uniform measure; integer WHT gives
    a_S = 2^n fhat(S); weights w_S = a_S^2/4^n exact Fractions.
  * H = sum over ALL S (incl. emptyset) of w_S log2(1/w_S).  LOG BASE 2.
  * I = sum_S w_S |S| (= average sensitivity), exact Fraction.
  * Parseval sum w_S == 1 asserted; all verdicts are exact rational
    comparisons of interval endpoints. No float enters any decision.
  * Amplification: O'Donnell-Tan 2013 Lemma 5.1 / Hod 2017 Prop 1.2 --
    g balanced (fhat(0)=0 exactly), H[g] > 0, then C_71 >= H[g]/(I[g]-1).
    Both hypotheses are verified below, never assumed.

USAGE:  python3 check_c71.py [--dps N]     # selftest + all five certificates
        python3 check_c71.py --selftest    # anchors only
Exit 0 iff selftest passes and ALL FIVE bounds are CERTIFIED.
"""
import sys
from fractions import Fraction

import mpmath
from mpmath import iv

RECORD = Fraction(64547837166, 10**10)  # beta(1/2) < 6.4547837166 (fine bar; the
# published table bar 6.4547837 = 64547837/10^7 is weaker and implied)
RECORD_STR = "6.4547837166"  # display form of RECORD (exact)

# Truth tables as TRUE(-1)-set bitmasks: bit x of the integer = input index x.
CERTS = [
    {
        "name": "n=14 g14 (headline record, logic-monotone)",
        "n": 14,
        "truth_table_true_hex": (
            "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00"
            "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00"
            "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00"
            "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00"
            "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00"
            "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00"
            "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000"
            "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f0c0000000000000000000"
            "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00"
            "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00"
            "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00"
            "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00"
            "fefefefef0f0f000faaafaaaf0a0f000fefeccccf0f000000000000000000000"
            "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00"
            "fefefeeef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00"
            "fefefeeef0f0f000faaafaaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefeeef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000"
            "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefeeef0f0f000faaafaaaf000f000fefeccccf0f000000000000000000000"
            "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00"
            "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc00feaacc00"
            "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00"
            "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00eeaacc00eeaacc00"
            "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00"
            "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000"
            "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc00feaacc00"
            "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000"
            "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefeeefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00"
            "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00feaacc00feaacc00"
            "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00"
            "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc00eeaacc00"
            "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000"
            "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00"
            "fefefeeef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000"
            "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00feaacc00feaacc00"
            "fefefeeef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000"
            "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefeeef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefeeefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefeeef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000"),
        "claimed_I": "521/256",
        "monotone": True,   # exhaustively re-verified below before certifying
        "claimed_value_prefix":
            "6.49011284352339435967722960726821776674269968263998854502375",
    },
    {
        "name": "n=12 g12* (secondary exhibit, logic-monotone)",
        "n": 12,
        "truth_table_true_hex": (
            "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00"
            "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefefe00feaafeaafeaafe00fefeccccfefecc00feaacc88feaacc00"
            "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00"
            "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefefc00feaafeaafeaafc00fefeccccfefecc00eeaacc88eeaacc00"
            "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00"
            "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000"
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00feaacc88feaacc00"
            "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000"
            "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00"
            "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f000000000000000000000"
            "fefefefefefafc00feaafeaafeaafc00fefeccccfefacc00eeaacc88eeaacc00"
            "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000"),
        "claimed_I": "259/128",
        "monotone": True,   # exhaustively re-verified below before certifying
        "claimed_value_prefix":
            "6.47606682836897279657734782555743832480092248239414132791560",
    },
    {
        "name": "n=12 (secondary exhibit, logic-monotone)",
        "n": 12,
        "truth_table_true_hex": (
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00"
            "fefefefef0f0f000feaafeaaf0a0f000fefeccccf0f0c0000000000000000000"
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00"
            "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefefef0f0f000feaafeaaf0a0f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefefef0f0f000faaafaaaf0a0f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00"
            "fefefefef0f0f000feaafeaaf000f000fefeccccf0f0c0000000000000000000"
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00"
            "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000"
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc00eeaacc00"
            "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f000000000000000000000"),
        "claimed_I": "259/128",
        "monotone": True,   # exhaustively re-verified below before certifying
        "claimed_value_prefix":
            "6.47420551506326097672878905526134366478869341423326622617201",
    },
    {
        "name": "n=11 (secondary exhibit)",
        "n": 11,
        "truth_table_true_hex": (
            "f0f33337f7f000f000f555f555f000f0f0f7f7f7f7f0033557f0033557f00337"
            "f7f33337f7f007f557f557f557f007f7f7f7f7f7f7f000000000000000000000"
            "f0f33337f7f000f000f555f555f000f0f0f7f7f7f7f0033557f0033557f00335"
            "f7f33337f7f007f557f557f557f007f5f7f7f7f7f7f000000000000000000000"
            "f0f33337f7f000f050f555f555f000f0f0f777f7f7f0033557f0033557f00337"
            "f7f33337f7f007f557f557f557f007f7f7f777f7f7f000000000000000000000"
            "f0f33337f7f000f050f555f555f000f0f0f777f7f7f0033557f0033557f00335"
            "f7f33337f7f007f557f557f557f007f5f7f777f7f7f"),
        "claimed_I": "129/64",
        "monotone": False,
        "claimed_value_prefix":
            "6.46774604903207696483653989653517242017762893521060811040418",
    },
    {
        "name": "n=10 (monotone representative)",
        "n": 10,
        "truth_table_true_hex": (
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00"
            "fefefefef0f0f000feaafeaaf000f000fcfcccccf0f0c0000000000000000000"
            "fefefefefefafe00feaafeaafeaafe00fefeccccfefacc00eeaacc88eeaacc00"
            "fefefefef0f0f000faaafaaaf000f000fcfcccccf0f0c0000000000000000000"),
        "claimed_I": "257/128",
        "monotone": True,   # exhaustively re-verified below before certifying
        "claimed_value_prefix":
            "6.45937228163785573157436161221912416621861332113900446566553",
    },
]


# ------------------------------------------------------------------ exact core
def wht(table):
    a = list(table)
    h = 1
    while h < len(a):
        for i in range(0, len(a), 2 * h):
            for j in range(i, i + h):
                x, y = a[j], a[j + h]
                a[j], a[j + h] = x + y, x - y
        h *= 2
    return a


def spectrum(table):
    N = len(table)
    a = wht(table)
    w = {s: Fraction(c * c, N * N) for s, c in enumerate(a) if c != 0}
    assert sum(w.values()) == 1, "Parseval failed: sum w_S != 1"
    return w, a[0]


def influence(weights):
    return sum(wS * bin(s).count("1") for s, wS in weights.items())


def table_from_hex(n, true_hex):
    mask = int(true_hex, 16)
    assert mask < (1 << (1 << n))
    return [-1 if (mask >> x) & 1 else 1 for x in range(1 << n)]


def is_logic_monotone(table, n):
    """Exhaustive: flipping any input FALSE->TRUE (setting bit i, since
    TRUE = -1) never turns the output TRUE(-1) -> FALSE(+1)."""
    for i in range(n):
        b = 1 << i
        for x in range(1 << n):
            if not x & b and table[x] == -1 and table[x | b] == +1:
                return False
    return True


# ------------------------------------------------------------ interval helpers
def iv_frac(q):
    return iv.mpf(int(q.numerator)) / iv.mpf(int(q.denominator))


def endpoint_frac(raw):
    sign, man, exp, _ = raw
    if man == 0:
        return Fraction(0)
    v = Fraction(man) * (Fraction(2) ** exp)
    return -v if sign else v


def entropy_interval(weights):
    H = iv.mpf(0)
    ln2 = iv.log(2)
    for wS in weights.values():
        if wS == 1:
            continue
        H += iv_frac(wS) * (iv.log(int(wS.denominator)) - iv.log(int(wS.numerator))) / ln2
    return H


def h_interval(q):
    if q == 0 or q == 1:
        return iv.mpf(0)
    return entropy_interval({0: q, 1: 1 - q})


# -------------------------------------------------------------- the certificate
def check_cert(cert):
    n = cert["n"]
    table = table_from_hex(n, cert["truth_table_true_hex"])
    if cert["monotone"]:
        assert is_logic_monotone(table, n), "monotone claim FAILS"
    weights, a0 = spectrum(table)
    I = influence(weights)
    assert I == Fraction(cert["claimed_I"]), f"I mismatch: computed {I}"
    assert a0 == 0, "amplified ratio requires a balanced function (fhat(0)=0)"
    assert I > 1, "amplified ratio requires I > 1"
    H = entropy_interval(weights)
    ratio = H / iv_frac(I - 1)
    lo, hi = endpoint_frac(ratio._mpi_[0]), endpoint_frac(ratio._mpi_[1])
    assert endpoint_frac(H._mpi_[0]) > 0, "H > 0 hypothesis"
    claimed = Fraction(*_dec(cert["claimed_value_prefix"]))
    ok = (lo > RECORD) and (claimed <= lo)
    print(f"{cert['name']}: n={n}, balanced (fhat(0)=0): True, I = {I}, "
          f"monotone = {cert['monotone']}")
    print(f"  C = H/(I-1) certified in [{_floor(lo, 30)}..., {_ceil(hi, 30)}...]")
    print(f"  claimed (floor-truncated)  {cert['claimed_value_prefix']}")
    print(f"  claimed <= lower endpoint: {claimed <= lo};  "
          f"lower endpoint > {RECORD_STR} (> beta(1/2)): {lo > RECORD}")
    print("  CERTIFIED" if ok else "  NOT CERTIFIED")
    return ok


def _dec(s):
    a, b = s.split(".")
    return int(a + b), 10 ** len(b)


def _floor(fr, k):
    sc = fr * 10 ** k
    s = str(sc.numerator // sc.denominator)
    return s[:-k] + "." + s[-k:]


def _ceil(fr, k):
    sc = fr * 10 ** k
    s = str(-((-sc.numerator) // sc.denominator))
    return s[:-k] + "." + s[-k:]


# ------------------------------------------------------------------- selftest
def beta_half_interval(K=220):
    """Hod Thm 4.4 incumbent beta(1/2): exact q-ladder, interval h, certified
    geometric tail (q_j <= 2/3 for j >= 2 at z = 1/2 -> tail <= pi_K * 2)."""
    z = Fraction(1, 2)
    qs = [z]
    for _ in range(K + 2):
        qs.append(1 / (1 + qs[-1]))
    S = h_interval(qs[0]) / iv_frac(1 - z) + h_interval(qs[1]) / iv_frac(z)
    pi = Fraction(1)
    for k in range(0, K + 1):
        if k >= 1:
            pi *= qs[k]
        S += h_interval(qs[k + 2]) * iv_frac(pi)
    r = max(qs[K + 1], qs[K + 2])
    S += iv_frac(pi * r / (1 - r)) * iv.mpf([0, 1])
    return S  # 4 z (1-z) = 1 at z = 1/2


def selftest():
    failures = []
    maj3 = [-1 if bin(x).count("1") >= 2 else 1 for x in range(8)]
    w, a0 = spectrum(maj3)
    H = entropy_interval(w)
    ok = (a0 == 0 and influence(w) == Fraction(3, 2)
          and endpoint_frac(H._mpi_[0]) <= 2 <= endpoint_frac(H._mpi_[1]))
    print(f"selftest Maj3:  I = {influence(w)} (want 3/2), H brackets 2: "
          f"{'PASS' if ok else 'FAIL'}")
    if not ok:
        failures.append("Maj3")

    b = beta_half_interval()
    blo, bhi = endpoint_frac(b._mpi_[0]), endpoint_frac(b._mpi_[1])
    ok = (Fraction(645478371656, 10**11) < blo <= bhi < Fraction(645478371657, 10**11)
          and bhi < RECORD)
    print(f"selftest beta(1/2) in [{_floor(blo, 12)}, {_ceil(bhi, 12)}] "
          f"(want 6.45478371656..., < {RECORD_STR}): {'PASS' if ok else 'FAIL'}")
    if not ok:
        failures.append("beta(1/2)")
    print("SELFTEST", "PASS" if not failures else f"FAIL: {failures}")
    return not failures


def main(argv):
    dps = 120
    if "--dps" in argv:
        i = argv.index("--dps")
        dps = int(argv[i + 1])
    iv.dps = dps
    mpmath.mp.dps = dps
    ok = selftest()
    if "--selftest" in argv:
        return 0 if ok else 1
    for cert in CERTS:
        ok = check_cert(cert) and ok
    print("ALL CERTIFIED" if ok else "FAILURE")
    return 0 if ok else 1


if __name__ == "__main__":
    sys.exit(main(sys.argv[1:]))

Exact commands:

pip install mpmath          # only dependency
python3 check_c71.py        # selftest, then all five certificates; exit 0
python3 check_c71.py --selftest   # anchors only: Maj3 (I = 3/2, H = 2 exactly);
                                  #   beta(1/2) = 6.45478371656... (the incumbent)
python3 check_c71.py --dps 240    # doubled precision; same verdict, same digits

Expected output (pasted from a real run, 2026-06-11, exit code 0):

selftest Maj3:  I = 3/2 (want 3/2), H brackets 2: PASS
selftest beta(1/2) in [6.454783716562, 6.454783716563] (want 6.45478371656..., < 6.4547837166): PASS
SELFTEST PASS
n=14 g14 (headline record, logic-monotone): n=14, balanced (fhat(0)=0): True, I = 521/256, monotone = True
  C = H/(I-1) certified in [6.490112843523394359677229607268..., 6.490112843523394359677229607269...]
  claimed (floor-truncated)  6.49011284352339435967722960726821776674269968263998854502375
  claimed <= lower endpoint: True;  lower endpoint > 6.4547837166 (> beta(1/2)): True
  CERTIFIED
n=12 g12* (secondary exhibit, logic-monotone): n=12, balanced (fhat(0)=0): True, I = 259/128, monotone = True
  C = H/(I-1) certified in [6.476066828368972796577347825557..., 6.476066828368972796577347825558...]
  claimed (floor-truncated)  6.47606682836897279657734782555743832480092248239414132791560
  claimed <= lower endpoint: True;  lower endpoint > 6.4547837166 (> beta(1/2)): True
  CERTIFIED
n=12 (secondary exhibit, logic-monotone): n=12, balanced (fhat(0)=0): True, I = 259/128, monotone = True
  C = H/(I-1) certified in [6.474205515063260976728789055261..., 6.474205515063260976728789055262...]
  claimed (floor-truncated)  6.47420551506326097672878905526134366478869341423326622617201
  claimed <= lower endpoint: True;  lower endpoint > 6.4547837166 (> beta(1/2)): True
  CERTIFIED
n=11 (secondary exhibit): n=11, balanced (fhat(0)=0): True, I = 129/64, monotone = False
  C = H/(I-1) certified in [6.467746049032076964836539896535..., 6.467746049032076964836539896536...]
  claimed (floor-truncated)  6.46774604903207696483653989653517242017762893521060811040418
  claimed <= lower endpoint: True;  lower endpoint > 6.4547837166 (> beta(1/2)): True
  CERTIFIED
n=10 (monotone representative): n=10, balanced (fhat(0)=0): True, I = 257/128, monotone = True
  C = H/(I-1) certified in [6.459372281637855731574361612219..., 6.459372281637855731574361612220...]
  claimed (floor-truncated)  6.45937228163785573157436161221912416621861332113900446566553
  claimed <= lower endpoint: True;  lower endpoint > 6.4547837166 (> beta(1/2)): True
  CERTIFIED
ALL CERTIFIED

Each certificate was checked by four independent code paths (zero shared
math code between any two of them), all exit 0 on the final certificates:

  1. Official project verifier (fei_verify.py) — integer fast WHT,
    exact Fraction influence, interval entropy at dps ≥ 100, Parseval enforced;
    balance and $I&gt;1$ preconditions gate the amplified bound; beats_record true
    for all five (the headline verified at dps = 130; its certificate
    c71_certificate_n14.json in the gist IS the verifier's output, itself
    re-checked).
  2. Independent checker (fei_check.py) — recursive-cofactor
    Fourier (no butterfly), edge-boundary/average-sensitivity influence (no
    Fourier), recomputation at higher dps with interval-containment checks;
    exit 0 on all five final certificates.
  3. Exact rescore during the search (a separate WHT + interval entropy from
    exact rationals, run on every hit before certification; for the $n = 14$ and
    $n = 12$ objects, the certificate generator additionally asserted exhaustive
    logic-monotonicity, exact balance and Parseval at creation time).
  4. Adversarial audits (independent agents, everything rebuilt from
    scratch, zero imports from any verifier above): for $g_{11}$/$g_{10}$,
    adversarial_audit_independent.py; for the $n = 12$ objects, fourth-line
    audits (audit_burst_fourthline.py for $g_{12}$, report
    ADVERSARIAL_AUDIT_BURST.md; audit_burst_fourthline_overnight.py for
    $g_{12}^{\star}$); for the headline $g_{14}$, a dedicated fourth-line audit
    (audit_ridge_fourthline_n14.py — the same independent machinery on the
    adapted input, plus the exact-rational cross-cert comparison
    $C_{\mathrm{lo}}(g_{14}) - C_{\mathrm{hi}}(g_{12}^{\star}) = +1.4046\cdot 10^{-2} &gt; 0$
    against the old certificate's UPPER enclosure endpoint, plus adversarial
    perturbation tests as negative controls: a single-entry flip, a balanced
    pair swap, a monotonicity tamper, a bumped quoted digit and an inflated
    record bar are each correctly rejected by the corresponding check) — two
    independent WHTs (direct $O(N^2)$ + butterfly, plus a third spot-check
    route), two influence routes (spectral + edge-boundary), two entropy routes
    (mpmath intervals at dps = 130 AND pure-rational range-reduced atanh-series
    log bounds with explicit remainders), independent $\beta(1/2)$ recomputation
    with certified tail, exact rational verdict path throughout, exhaustive
    monotonicity over all comparable pairs (covering pairs AND full $3^n$ subset
    enumeration), digit-by-digit floor-truncation verification of every quoted
    string, machine check of the amplification identities on a concrete seed,
    and NPN known-family exclusion. Exit 0.

The standalone check_c71.py above is a fifth, self-contained path (derived from
the project's checker template, certificates inlined) intended for the reviewer.

Standard caveats

  • Bound type: finite balanced seed + O'Donnell–Tan Prop 1.2 self-composition —
    the same mechanism as the page's existing 6.278944 entry [OT2013]. The bound
    certifies $C \ge H/(I-1)$ as a supremum of finite-function ratios
    ($H[f_m]/I[f_m] = (H/(I-1))(1-I^{-m})$, strictly increasing); no single finite
    function attains it. This matches how the existing OT2013 row is quoted.
  • Quoted digits are downward-truncated. Every decimal string in this PR is an
    exact floor-truncation of the certified interval's lower endpoint, never a
    nearest-rounded float. (Process note: an earlier internal version of the
    certificate JSONs had their final 59th digit nearest-rounded by the formatting
    path of the project verifier; this was caught by the adversarial audit and the
    certificates regenerated — no quoted digit anywhere in this PR comes from that
    path. The 16- and 30-digit headline values were always valid truncations. The
    fourth-line audit of $g_{14}$ re-verified every quoted digit string of the
    headline certificate to be floor-exact, digit by digit, against its own
    independently derived enclosures.)
  • Monotone framing: the headline $g_{14}$ is logic-monotone as
    shipped
    (exhaustively verified, no reorientation), so the general and
    monotone-class bounds coincide at $6.4901\ldots$ in one certificate. Among the
    secondary exhibits, $g_{12}^{\star}$ and $g_{12}$ are likewise logic-monotone
    as shipped, $g_{10}$
    is monotone via the representative actually shipped (the
    search-orientation table is its global input negation — stated explicitly
    above), and $g_{11}$ carries no monotone claim.
  • The known upper-bound side is unchanged: no finite universal constant is known
    ($C_{71} \le \infty$); within read-once formulas the ceiling is $C \le 10$
    [OT2013; CKLS2015], so the new value is consistent with all known upper bounds.
  • $H/I$ vs $H/(I-1)$: the claimed bounds are $H/(I-1)$ for exactly balanced
    functions via OT 2013 Prop 1.2 (Lemma 5.1), as stated and hypothesis-checked
    above. The raw ratios $H/I \approx 3.301, 3.276, 3.275, 3.26, 3.24$ appear only
    inside the certificates' ratio_interval field and are never claimed as bounds.

AI assistance disclosure

This is a fully AI-derived result: the construction was found and certified by
Mosaic Intelligence's automated search-and-verification system, and the
submission text was AI-prepared. All numerical results and references were
independently re-run and verified before submission.

@463464q435q43 463464q435q43 force-pushed the improve-71-lower-bound branch from 4c41208 to e33b2df Compare June 10, 2026 17:01
@463464q435q43 463464q435q43 changed the title Improve lower bound for C_71 Improve lower bound for C_71 to 6.4760668283689727 Jun 11, 2026
@463464q435q43 463464q435q43 changed the title Improve lower bound for C_71 to 6.4760668283689727 Improve lower bound for C_71 to 6.4901128435233943 Jun 11, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant