OAI/NumberTheory/TwoPoint/Walks/WitnessMetadata.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.internal_witness_metadata line 12
2. theorem OAI.TwoPointCorrelations.witness_system_metadata line 38

   Source documentation

   Every index in the constructed metadata is bounded by the total recorded-length bound. Thus the actual four-way selector is covered by the finite code count, with no numerical-prime values in its code.

   theorem witness_system_metadata {n K h s J N : ℕ} {supply : ℕ → ℕ → Prop}
       {ι : Type*} [DecidableEq ι]
       (main : LabeledPrimeWord ι) (word : Fin n → LabeledPrimeWord ι)
       (value : ι → ℕ) (hinj : Function.Injective value) (hprime : ∀ j, (value j).Prime)
       (hm : main.Realizes value) (hw : ∀ i, (word i).Realizes value)
       (mark : Fin n → ι) (attachment position : Fin n → ℕ)
       (hsize : 8 * K ≤ n)
       (hminimal : ∀ i, MinimalWord (ForwardProhibited h s supply) (word i).word)
       (hsq : ∀ i t, t ∈ (word i).word → Squarefree t.tuple)
       (hcard : ∀ i t, t ∈ (word i).word → t.tuple.primeFactors.card = J)
       (hsupport : ∀ i p j, TuplePrimeAt (word i).word p j →
         ¬p ∣ h ∧ ∀ t ∈ (word i).word, ¬p ∣ t.padding)
   …

   Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.MinimalWord, OAI.TwoPointCorrelations.ForwardProhibited, OAI.TwoPointCorrelations.TuplePrimeAt