Nontermination

Statements for paper Section 5: Theorem 5.1 (thm:membership), Theorem 5.2 (thm:main) and the nontermination corollary, together with the injectable-set characterization of Appendix A. Proofs are deferred.

Formalization boundary: the recursively expressible hierarchy I^exp_t (paper Definition 2.5, and Lemma 5.10 (lem:expressible) of Section 5.3) is not formalized; see the header of Defs.lean. The paper's Q(ε,r) ∈ I^exp_t ⊆ I^AI_t ⊆ I^NW_t is formalized here as its two weaker halves, membership in I^AI_t and in I^NW_t.

Auxiliary facts

These are general facts that the proofs below need and that the imported files do not state; they are proved here privately.

The two formalized hierarchies

theorem TriangleInflation.nwFeasible_of_aiFeasible {t : ℕ} {P : ThreeBit → ℝ} (h : AIFeasible t P) : NWFeasible t P

Paper equation (eq:nested), the part that the formalized definitions express: I^AI_t ⊆ I^NW_t.

theorem TriangleInflation.injectable_iff_injectableRaw {t : ℕ} (ht : 1 ≤ t) (S : Finset (Obs t)) : Injectable S ↔ InjectableRaw S

Paper Appendix A.3 (app:injectable): for the triangle, the injectable sets of the order-t inflation are exactly the subsets of copied triangles.

Theorem 5.1: membership at every finite order

theorem TriangleInflation.defectLaw_witnesses_AI (t : ℕ) {ε r : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (hr0 : 0 ≤ r) (hr1 : r ≤ (1 - ε) ^ (t - 1)) : IsLaw (defectLaw t ε (sParam t ε r)) ∧ SymmetricLaw t (defectLaw t ε (sParam t ε r)) ∧ pushforward (defectLaw t ε (sParam t ε r)) readDiagonal = tensorPow t (Q ε r) ∧ InjectableMarginals t (defectLaw t ε (sParam t ε r)) (Q ε r) ∧ AncestralProducts t (defectLaw t ε (sParam t ε r)) (Q ε r)

The defect law with s = 1 - r/(1-ε)^{t-1} witnesses the ancestral-independence conditions for Q(ε,r): this is the content of paper Section 5.3 for the two formalized hierarchies.

theorem TriangleInflation.membership_AI (t : ℕ) {ε r : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (hr0 : 0 ≤ r) (hr1 : r ≤ (1 - ε) ^ (t - 1)) : AIFeasible t (Q ε r)

Paper Theorem 5.1 (thm:membership), ancestral-independence half: for t ≥ 1, 0 < ε < 1 and 0 ≤ r ≤ (1-ε)^{t-1}, the law Q(ε,r) is feasible at order t for the ancestral-independence hierarchy.

theorem TriangleInflation.membership_NW (t : ℕ) {ε r : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (hr0 : 0 ≤ r) (hr1 : r ≤ (1 - ε) ^ (t - 1)) : NWFeasible t (Q ε r)

Paper Theorem 5.1 (thm:membership), Navascués–Wolfe half.

Theorem 5.2: no finite characterizing order

theorem TriangleInflation.epsFam_mem (t : ℕ) (ht : 1 ≤ t) : 0 < epsFam t ∧ epsFam t < 1

The parameters of paper Theorem 5.2 lie in the range of Theorem 5.1.

theorem TriangleInflation.main_membership (t : ℕ) (ht : 1 ≤ t) : AIFeasible t (Pfam t) ∧ NWFeasible t (Pfam t)

Paper Theorem 5.2 (thm:main), membership half: P_t ∈ I^AI_t ⊆ I^NW_t.

theorem TriangleInflation.main_violation (t : ℕ) (ht : 1 ≤ t) : epsFam t ^ 2 / 2 ≤ atom000 (Pfam t) ^ 2 - margA (Pfam t) * margB (Pfam t) * margC (Pfam t) ∧ ¬TriangleCompatible (Pfam t)

Paper Theorem 5.2 (thm:main), violation half: the Finner margin of P_t is at least ε_t²/2 > 0, so P_t ∉ C_tri.

theorem TriangleInflation.Pfam_isLaw (t : ℕ) (ht : 1 ≤ t) : IsLaw (Pfam t)

P_t is a probability law.

theorem TriangleInflation.no_finite_characterizing_order_lib (t : ℕ) (ht : 1 ≤ t) : ∃ (P : ThreeBit → ℝ), IsLaw P ∧ AIFeasible t P ∧ NWFeasible t P ∧ ¬TriangleCompatible P

Paper Theorem 5.2 (thm:main), the nontermination corollary: for every finite order t there is a three-bit law that passes the order-t test and is not triangle compatible, so no finite order of the hierarchy characterizes C_tri.

The plain name TriangleInflation.no_finite_characterizing_order is reserved for the registry statement, which PalomarSolutions/TriangleInflation.lean declares and discharges by this theorem; Comparator identifies the Challenge and the Solution by that one name.