📋 AUDIT: all hypothesis-gated unproven propositions beyond the single declared Vitali axiom

[phasetr]

Exhaustive audit (2026-06-24) of every proposition in the GJ §17–18 formalization that is not actually proven, beyond the single deliberately-declared axiom. Performed by a Lean.collectAxioms whole-environment sweep + an independent claude -p source audit cross-checked against docs/index.md.

Level-0 confirmations (axioms / sorry / native_decide)

• Real axiom declarations: exactly one — FunctionTheory.vitaliPorter_tendstoLocallyUniformlyOn (IsingModel/ComplexAnalyticity/FunctionTheoryAxioms.lean:54). The other axiom-keyword grep hits (Phi4.lean:144, HighTempMassGap.lean:311, Contraction.lean:885) are doc-comment prose describing former-and-now-deleted/proven axioms, not declarations.
• sorry / admit: none in code (the two grep hits are doc-comment prose).
• native_decide (→ Lean.ofReduceBool): none in named library theorems — only in example sanity checks (TestGenerators.lean, test/**).
• Definitive #print axioms on headline capstones across all chapters (verified directly):
  • ghs_inequality (§4) → [propext, Classical.choice, Quot.sound]
  • peierls_spontaneous_magnetization_pos_cubic (§17.x Peierls) → standard 3 only
  • clusterExpansion_supersedes_transferMatrix_gap (§17.1 item B) → standard 3 only
  • gibbsExpectationBC_originObs_cubicExhaustion_boundary_influence_uniform, plusStateExpectation_eq_minusStateExpectation_originObs, tendsto_gibbsExpectationBC_originObs_free_limit, plusStateExpectation_eq_minusStateExpectation, tendsto_gibbsExpectationBC_localObs_free_limit, gibbsExpectationBC_minus_volume_monotone (§17.1 Dobrushin uniqueness) → standard 3 only
  • truncated2Infinite_latticeGraph_tendsto_atTop_zero_of_high_temp (§5.1, B7) → standard 3 only
  • correlationInfinite_latticeGraph_two_point_analytic_high_temp (§18.6/§18.7 item D) → [propext, Classical.choice, Quot.sound, vitaliPorter] — i.e. standard 3 plus only the disclosed Vitali axiom.
    No sorryAx, no Lean.ofReduceBool, no other axiom in any checked capstone. (A whole-collectAxioms environment sweep was attempted but is impractically slow on the full env; the per-capstone #print axioms above is the definitive check.)

So "axiom-free except vitaliPorter" is literally true at the axiom/sorry/native_decide level. The genuine remaining gaps are hypothesis-gated: a deep GJ/FV proposition carried as an undischarged Prop/structure-field rather than proven.

A. The one declared axiom (disclosed, deliberate)

• A1 — Vitali–Porter local-uniform convergence — vitaliPorter_tendstoLocallyUniformlyOn (FunctionTheoryAxioms.lean:54). Feeds §18.6/§18.7 (item D). Research-level / scope policy.

B. Genuine hypothesis-gated unproven book propositions — one tracking issue each

#	Proposition	Lean carrier (file:line)	GJ §	Tractability
B1	§17.5 adjacent-pair exponential-decay bridge	PseudoMassLatticeDistanceBridge (PseudoMass/HLSCorrelationCapstone.lean:46)	§17.5	research
B2	§17.5/§18.6 volume-uniform complex CE inputs	VolumeUniformComplexHTBound / VolumeUniformZComplexIdentity (AmbientComplexAnalyticity/VolumeUniformHZ.lean:50,69)	§18.6	research
B3	§17.5 tanh decay profile	cubicTanhProfileBound (Concrete/.../CubicPseudoMassBasic.lean:89)	§17.5	research
B4	§17.5 sharp HLS constant (Thm 17.5.1)	conditional scaffolding only (non-sharp sandwich IS proven)	§17.5	research
B5	§17.5/§17.8 d≥2 correlation-length / anomalous-dim continuity	no general-d Lean version (strip-only proven)	§17.5/§17.8	research
B6	§5.1/§17.1 cluster property for general pure phases	clusterProperty_…_of_polynomialDecay (PR #958), gated on HasPolynomialDecay	§5.1/§17.1	research
B7	§5.1/§17.4 distance cluster decay, Summable-gated	truncated2Infinite_latticeGraph_tendsto_atTop_zero_of_summable (Concrete/.../CorrelationDecay.lean:80)	§5.1	tractable (1 PR)

C. Documented-and-superseded scaffolding — NOT live gaps (recorded to prevent false positives)

• C1 §4.6 Thm 4.6.2 infinite-volume "Vitali" block (~100 *_vitali_bridge* rows, docs/index.md:1495–1593): superseded — GJ Thm 4.6.2 is fully proven by a different route (freeEnergyComplex_infiniteVolume_analyticOnNhd_leeYangDomain, PR feat(gj-4.6.2): real-axis identification and domain globalisation — Thm 4.6.2 (final) — #628 #3905), needing only 0<β,0<J.
• C2 transfer-matrix transverse-volume-uniform spectral-gap certificates (LayerSpectralGapCertificate etc.): the theta_lt_one field is the documented obstruction (TransferMatrix/ClusterExpansionSupersession.lean:13), superseded by the §18 cluster-expansion route (PR feat(gj-17.1): §18 cluster expansion supersedes the transfer-matrix infinite-volume gap — #4214 (B-ii) #4228). Only the general-d continuity consequence (= B5) is a live gap.
• Benign preconditions (0≤J, 0<β, βJ·2d<1, ferromagnetic, finiteness, distinct sites, Fekete DisjointTowerHypotheses, RealOrthogonalSpectralData, etc.) are legitimate hypotheses, not gaps.

Tracking (sub-issues filed)

• A1 Vitali axiom — disclosed; scope doc in FunctionTheoryAxioms.lean (no separate issue, deliberate).
• B1 GJ §17.5: volume-uniform adjacent-pair exponential-decay bridge (PseudoMassLatticeDistanceBridge) — UNPROVEN #4268 — adjacent-pair exp-decay bridge (§17.5, research)
• B2 GJ §18.6/§17.5: volume-uniform complex cluster-expansion inputs (single uniform disc) — UNPROVEN #4269 — volume-uniform complex CE inputs (§18.6, research)
• B3 GJ §17.5: pseudo-mass tanh decay profile (cubicTanhProfileBound) — UNPROVEN #4270 — tanh decay profile (§17.5, research)
• B4 GJ §17.5: SHARP HLS constant / Theorem 17.5.1 (master #4214 item C) — UNPROVEN #4271 — SHARP HLS constant / Thm 17.5.1 = master GJ §17–18 Ising formalization — FULL COMPLETION tracker (master) #4214 item C (research)
• B5 GJ §17.5/§17.8: d≥2 correlation-length / anomalous-dimension continuity (transverse-uniform spectral gap) — UNPROVEN #4272 — d≥2 correlation-length continuity (§17.5/§17.8, research)
• B6 GJ §5.1/§17.1: cluster property for general pure phases (HasPolynomialDecay-gated) — UNPROVEN #4273 — high-temperature discharge of the polynomial-decay hypothesis (§17.8/§5.1) — DONE (feat(gj-17.8): discharge polynomial-decay hypothesis at high temperature — closes #4273 (audit B6) #4276, main d31fbbd4): hasPolynomialDecay_latticeGraph_of_betaJ_two_d_lt_one promotes the GJ (17.8.1) hypothesis to a theorem at βJ·2d<1; §17.8 η≤1 + §5.1 cluster property as unconditional corollaries. (GJ assumes (17.8.1) as the scaling hypothesis — conditional forms faithful; low-T remains the genuine scaling hypothesis.)
• B7 GJ §5.1/§17.4: unconditional high-temperature distance cluster decay (discharge the Summable hypothesis) — TRACTABLE #4274 — high-temp distance cluster decay, discharge Summable (§5.1) — DONE (feat(gj-5.1): unconditional high-temperature distance cluster decay — closes #4274 (audit B7) #4275, main 6bed4cfd): truncated2Infinite_latticeGraph_tendsto_atTop_zero_of_high_temp, axiom-free

Master tracker #4214 updated to reflect §17.5 (item C) is not complete and B5/B6/B7 are additional open conditional propositions.