Physics

This lesson starts with a finite model: phases on directed graph edges, paths that add those phases, and closed loops whose endpoint gauge shifts cancel.

The ordinary baseline is lattice gauge notation. A link variable sits on an oriented edge, a path accumulates link values, and a Wilson loop records a closed-path quantity. Circle Calculus does not replace that notation. It adds a proof-status-safe interface:

finite edge diagram
  -> path record
  -> holonomy calculation
  -> gauge-transform certificate
  -> theorem and dictionary ids
  -> paper, Python, and Lean sidecars

This is a finite bookkeeping lesson: its diagrams and Python fixtures are executable references, not proofs, and it makes no claim about real physics (no electromagnetism, quantum field theory, Yang–Mills, or Berry phase). See What “Proved” Means Here.

Showcase evidence: SHOW-007 quaternion, Hopf, and phase coordinates; SHOW-008 proof-carrying finite gauge paths.

What You Should Learn

By the end of the page, you should be able to separate an open-path endpoint effect from a closed-loop Wilson certificate in a finite Z_n phase model, and explain why quaternion representatives q and -q can be distinct records with the same bounded conjugation action while pure-vector inputs stay inside the pure-vector boundary.

Ordinary Baseline

In standard lattice language, a gauge field assigns data to edges. A vertex gauge choice changes the local representatives. Closed-loop quantities are important because endpoint effects cancel around a loop.

That is already standard mathematics. The Circle Calculus contribution is not the idea of a Wilson loop. The contribution is the source-linked record that keeps the diagram, finite calculation, theorem id, dictionary ids, paper section, Python fixture, and Lean target together.

Circle Calculus Framing

The finite model reuses earlier vocabulary:

circle phase     -> edge phase modulo n
rotation sum     -> path holonomy
closure          -> closed loop
fiber choice     -> vertex gauge representative
certificate      -> source-linked status record

The visible path is the base object. The hidden phase choices live at vertices. For an open path, the source and target shifts remain visible. For a closed path, the endpoint is the same node, so those shifts cancel in the finite fixture.

Executable Fixture

The Python reference model under circle_math/physics.py provides:

GaugeEdge
GaugePath
path_holonomy
concat_paths
reverse_path
gauge_transform_path
transformed_holonomy_endpoint_prediction
square_plaquette_path
wilson_loop_certificate

The sidecar tests check a composable path, a reversed path, an open-path gauge transform, a closed Wilson loop, identity/two-path/three-path closed-loop records, gauge-shifted closed-loop records, one-step and two-step three-path basepoint rotations, open-path rejection for closed-loop records, and a square plaquette.

The first widget shows the path algebra before the closed-loop case: concatenate a composable path, reverse it, close it by following the reverse, and compare an open-path gauge transform against its endpoint prediction. It is finite bookkeeping only; the theorem cards remain the formal status source.

The second widget specializes that idea to a square plaquette. Change the edge phases or vertex gauge choices and compare the original holonomy with the transformed holonomy. It is not a proof and not a physics prediction.

The third widget turns the closed-loop calculation into a certificate-style record. It checks the same triangular Wilson loop under several sampled vertex gauges and records exactly which finite theorem cards support the closed-loop boundary.

The same finite idea now has a reusable ClosedGaugeLoop Lean record. The record stores a checked path plus the proof that its endpoints close, so identity-loop, two-path-cycle, and three-path-cycle holonomy facts can be linked directly to theorem cards instead of living only in prose.

The Hopf hidden-phase widget shows the next layer of the same idea: a visible base coordinate can stay fixed while a hidden circular phase changes the lifted S3 pair. This is a bounded coordinate fixture linked to S3 Hopf theorem cards, not a claim about Berry phase or a complete fiber-bundle formalization.

The next bounded physics-facing lesson moves from finite gauge loops to quaternion orientation debugging. Standard quaternion orientation code has a familiar sign ambiguity: q and -q are different representatives, but they should not be treated as different downstream orientations when the action being compared is quaternion conjugation. The widget below exposes exactly that finite algebraic claim, plus the Lean-checked fact that pure-imaginary quaternion inputs stay pure-imaginary after conjugation. It links both boundaries to the S3 spin theorem cards.

The periodic-dynamics lane stays even more modest. It records a stroboscopic finite phase, the lifted winding/residue of the total motion, the closure period from the gcd theorem, and a synthetic marked-defect loop with signed winding. This is a finite audit fixture for P7-PHYS-004, not Floquet theory, action-angle mechanics, or a continuum defect model.

If a path starts at s and ends at t, which gauge values survive after every interior vertex cancellation?

Proof Boundary

The theorem cards below are Lean-proved for the finite ZMod n phase and link-path model. The Python graph fixtures remain executable references. Their status comes from generated theorem data.

The Hopf cards are Lean-proved coordinate facts: normalized pairs land on the unit base equation, unit phase rotation preserves the visible base, and phase actions obey identity/composition laws. They do not prove Berry phase, quantum mechanics, or the full topology of the Hopf fibration.

The spin-sign cards are Lean-proved S3 algebraic facts. They support the bounded orientation-debugging widget, but they are not a full formalization of SO(3), robotics, spinors, or physical rotations.

Dictionary Trail

Source Trail

Physics paper: Proof-Carrying Finite Lattice Gauge Links

Bundle paper: Bundle Calculus

Hopf paper: Hopf Coils

Spin paper: Spin Double Cover Roadmap

Winding paper: Winding Naturals

The Python fixture is an executable reference. The current Lean model proves finite phase-list and link-path holonomy facts plus singleton, two-link, singleton-concat, three-link, four-link, empty-identity, concat-identity, concat-associativity, reversal-algebra, path-plus-reverse zero-holonomy gates, boundary-append composability, first source/target projection facts, checked finite path endpoint facts, checked finite path identity/associativity laws, checked finite path holonomy identity/singleton/concat laws, projection bridges from checked paths back to the link-path carrier, closed checked-path gauge-invariance facts, two-path and three-path cycle gauge-invariance certificates, and a reusable ClosedGaugeLoop record with identity/cycle holonomy, gauge-shifted holonomy, gauge-sample independence, and complete cyclic three-path basepoint rotation packages. A full finite graph path category remains future graph-path work.