physicallyEquivalent
This definition states that two ledger states encode identical physics when their complex entries differ solely by multiplication with a common phase factor exp(iθ) for some real θ. Gauge theorists and Recognition Science researchers would cite it as the precise origin of U(1) symmetry arising from ledger redundancy rather than imposed by hand. The definition is a direct existential quantification over the global phase with no additional lemmas required.
claimTwo ledger states $s_1$ and $s_2$ are physically equivalent when there exists a real number $θ$ such that the complex entries of $s_2$ equal the entries of $s_1$ each multiplied by $e^{iθ}$.
background
LedgerState is the structure that encodes physical reality as a finite list of complex entries together with a global phase; different representations of the same list are allowed to differ by that phase. The module QFT.GaugeInvariance derives gauge invariance directly from this redundancy in the ledger, treating the freedom to rotate all entries uniformly as the mathematical content of U(1) symmetry. Upstream structures such as Physical (minimal positivity assumptions on c, ħ, G) and the various LedgerState definitions in VariationalDynamics and InformationIsLedger supply the concrete data types that this equivalence relation acts upon.
proof idea
The declaration is a direct definition that encodes the global-phase relation via an existential quantifier over θ and a pointwise multiplication on the entry list; no tactics or lemmas are invoked beyond the built-in List.map and Complex.exp operations.
why it matters in Recognition Science
It supplies the base predicate for the three immediate downstream theorems that establish reflexivity, symmetry, and the explicit gauge-symmetry-from-redundancy statement. In the Recognition framework this definition realizes the core insight that gauge invariance equals information redundancy in the ledger, directly supporting the paper claim that U(1) symmetry emerges from RS ledger structure rather than being postulated. It sits downstream of the eight-tick octave and recognition composition law through the shared LedgerState representation.
scope and limits
- Does not define or prove invariance of observables under the equivalence.
- Does not extend the relation to local (position-dependent) gauge transformations.
- Does not connect the phase θ to specific physical charges or currents.
- Does not address multi-particle or field-theoretic extensions beyond the finite list of entries.
formal statement (Lean)
45def physicallyEquivalent (s1 s2 : LedgerState) : Prop :=
proof body
Definition body.
46 ∃ θ : ℝ, s2.entries = s1.entries.map (fun z => z * exp (I * θ))
47
48/-- **THEOREM**: Physical equivalence is an equivalence relation. -/