Foundation Primitive Recognition Calculus Grow Signed Orbit Nonneg Flag Mul Of Orbit Right Of Ne Zero Choice Free

A flag that survives multiplication

In the Recognition Science framework, the primitive recognition calculus is the basic algebra of how discrete recognition events combine. The framework models recognition as a ledger, a discrete record of events, and the calculus studies the operations that can be applied to such records. One central object is the signed orbit, a record that carries both a value and a sign flag indicating whether the record counts positively or negatively.

The module in question proves a theorem about what happens when you multiply a signed orbit by another orbit built from a nonzero distinction. A distinction is the framework's term for a basic unit of difference, and an orbit built from it is a record of that distinction's recognition history. The theorem states that the sign flag of the original signed orbit is unchanged by this multiplication: multiplying by any nonzero distinction's orbit does not flip the sign.

In symbols, the theorem reads: for any signed orbit z and any nonzero distinction d, the nonnegFlag of (z multiplied by the orbit of d) equals the nonnegFlag of z. The condition that d is nonzero is essential. The framework's choice-free requirement means the result holds for every signed orbit and every nonzero distinction, with no additional assumptions or choices made in the proof.

This result matters because it establishes a stability property at the very base of the framework's algebra. Before any complex structure is built, the calculus guarantees that sign information is preserved under a fundamental operation. This is a step toward showing that the framework's recognition algebra has consistent behavior, a property that later theorems in the forcing chain can rely on.

In Recognition Science, this theorem is one of the small, machine-checked building blocks. The framework's library, a machine-checked collection of formal theorems, records this proof as a theorem, meaning it has been verified by a computer to follow from the framework's axioms. It does not by itself establish the larger results of the framework, but it is a necessary piece of the foundation that those results stand on.

theorem nonnegFlag_mul_ofOrbit_right_of_ne_zero_cf
    (z : SignedOrbit) (d : DistinctionNat) (hd : d ≠ DistinctionNat.zero) :
    (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).nonnegFlag = z.nonnegFlag := by
  have hd' : d.toNat ≠ 0 := by
    intro h
    apply hd
    rw [← DistinctionNat.ofNat_toNat d, h, DistinctionNat.ofNat_zero]
  have hdpos : 0 < d.toNat := by omega
  have hpos : (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).pos.toNat = z.pos.toNat * d.toNat := by
    show (z.pos * (SignedOrbit.ofOrbit d).pos + z.neg * (SignedOrbit.ofOrbit d).neg).toNat = _
    have hp : (SignedOrbit.ofOrbit d).pos = d := rfl
    have hn : (SignedOrbit.ofOrbit d).neg = DistinctionNat.zero := rfl
    rw [hp, hn, DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_mul,
      DistinctionNat.toNat_zero]
    omega
  have hneg : (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).neg.toNat = z.neg.toNat * d.toNat := by
    show (z.pos * (SignedOrbit.ofOrbit d).neg + z.neg * (SignedOrbit.ofOrbit d).pos).toNat = _
    have hp : (SignedOrbit.ofOrbit d).pos = d := rfl
    have hn : (SignedOrbit.ofOrbit d).neg = DistinctionNat.zero := rfl
    rw [hp, hn, DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_mul,
      DistinctionNat.toNat_zero]
    omega
  have key : DistinctionNat.leq (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).neg
      (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).pos = true ↔
      DistinctionNat.leq z.neg z.pos = true := by
    rw [leq_eq_true_iff_cf, leq_eq_true_iff_cf, hpos, hneg]
    constructor
    · intro h
      exact Nat.le_of_mul_le_mul_right h hdpos
    · intro h
      exact Nat.mul_le_mul_right _ h
  show DistinctionNat.leq (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).neg
      (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).pos =
      DistinctionNat.leq z.neg z.pos
  cases hb : DistinctionNat.leq z.neg z.pos with
    | true => exact key.mpr hb
    | false =>
      cases hb2 : DistinctionNat.leq (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).neg
          (SignedOrbit.mul z (SignedOrbit.ofOrbit d)).pos with
        | true =>
          rw [key.mp hb2] at hb
          exact absurd hb (by decide)
        | false => rfl

What this page does not claim

This theorem by itself does not establish any of the framework's larger results such as the golden ratio or three spatial dimensions. The proof of this theorem does not require any choices to be made, but the framework's ambient type theory still supplies its own postulates. The sign flag preservation holds only for multiplication by a nonzero distinction, not for multiplication by zero.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/Grow/SignedOrbitNonnegFlagMulOfOrbitRightOfNeZeroChoiceFree.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: