`brgcPath_injective`

proved

show as: view math explainer →

module: IndisputableMonolith.Patterns.GrayCycleGeneral
domain: Patterns
line: 204 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Patterns.GrayCycleGeneral on GitHub at line 204.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 201
 202variable [GrayCodeFacts]
 203
 204theorem brgcPath_injective {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) : Function.Injective (brgcPath d) := by
 205  intro i j hij
 206  -- reduce to equality of the Nat Gray codes, then invert using `GrayCodeFacts.grayToNat_inverts_natToGray`.
 207  have hbits : ∀ k : Nat, (natToGray i.val).testBit k = (natToGray j.val).testBit k := by
 208    intro k
 209    by_cases hk : k < d
 210    · have := congrArg (fun p : Pattern d => p ⟨k, hk⟩) hij
 211      simpa [brgcPath, binaryReflectedGray, natToGray] using this
 212    · have hkge : d ≤ k := le_of_not_gt hk
 213      have hi0 : (natToGray i.val).testBit k = false :=
 214        natToGray_testBit_false_of_ge (d := d) (n := i.val) (k := k) i.isLt hkge
 215      have hj0 : (natToGray j.val).testBit k = false :=
 216        natToGray_testBit_false_of_ge (d := d) (n := j.val) (k := k) j.isLt hkge
 217      simp [hi0, hj0]
 218  have hgray : natToGray i.val = natToGray j.val := by
 219    exact Nat.eq_of_testBit_eq hbits
 220  -- show both indices are < 2^64
 221  have hpow : 2 ^ d ≤ 2 ^ 64 := Nat.pow_le_pow_right (by decide : 0 < (2 : Nat)) hd
 222  have hi64 : i.val < 2 ^ 64 := lt_of_lt_of_le i.isLt hpow
 223  have hj64 : j.val < 2 ^ 64 := lt_of_lt_of_le j.isLt hpow
 224  have hi_inv : GrayCodeAxioms.grayInverse (natToGray i.val) = i.val :=
 225    GrayCodeFacts.grayToNat_inverts_natToGray (n := i.val) hi64
 226  have hj_inv : GrayCodeAxioms.grayInverse (natToGray j.val) = j.val :=
 227    GrayCodeFacts.grayToNat_inverts_natToGray (n := j.val) hj64
 228  have : i.val = j.val := by
 229    have := congrArg GrayCodeAxioms.grayInverse hgray
 230    simpa [hi_inv, hj_inv] using this
 231  exact Fin.ext this
 232
 233lemma brgc_oneBit_step {d : Nat} (hdpos : 0 < d) (hd : d ≤ 64) :
 234    ∀ i : Fin (2 ^ d), OneBitDiff (brgcPath d i) (brgcPath d (i + 1)) := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.